COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%barwis[e89,jmc]		Comments on Barwise paper
C00007 ENDMK
C⊗;
%barwis[e89,jmc]		Comments on Barwise paper

Dear Jon,

	Here are some comments on your ``Mathematical Proofs of
Computer System Correctness'' which I found in a stack at CSLI.

	First a historical remark.  My first paper on this
subject was in 1961, long before Hoare, and I have been teaching
the subject at Stanford since 1962.  Bob Floyd wrote on the
subject in 1965.  However, the first proof of program correctness
was an informal one by Turing in 1948.  A Russian named Yanov
published a paper on the subject in 1958.  Dana Scott wrote on
the subject in 1969.  There are textbooks on program
verification, e.g. Zohar Manna's, which contain this history.
You ought to have referred to at least one actual textbook and
especially to have referred to the work of Robert Boyer and J
Moore.

	Second, proofs of program correctness do not usually take the
form of showing that a program realizes an algorithm.  They may
show input-output relations of the program, e.g. if the program variables
satisfy  P(x)  at the beginning, then they will satisfy  Q(x)
when the program is finished.  P  and  Q  may incorporate as
much or as little about program behavior as is convenient.
Another approach, used with Lisp programs, is to regard
the program as computing a function, and prove facts about
the function.  For example, the Lisp function  APPEND  is
proved associative, to have NIL as a left and right
identity and to have a certain relation to CONS.
The book by Boyer and Moore "A Computational Logic" is
quite sophisticated about some of these things.

	Third, in case of programs that interact with the
real world, e.g. air traffic control, matters are more
complex.  One can't say that the program implements an
algorithm in the sense of something with inputs and
outputs.  Instead there is an interaction between the
state of the program and the state of the world.
A proof of program correctness must involve assumptions
about physical processes taking place in the world.
The correctness of an air traffic control program
involves assumptions about the pilots obeying the
program and relations between what the pilots do
and the trajectories of the airplanes.

	Checking the proofs of program correctness by
computer is essential, because no-one will want to
check them by hand.  This was emphasized in my 1961 paper.
We built a sequence of logic proof checkers at Stanford
mainly for the purpose of checking proofs of program
correctness.  The most recent was Ketonen's EKL,
unfortunately abandoned when he left for Lucid to
make his fortune.

	I agree with your general point that program
verification is just another branch of applied mathematics.
People are accustomed to bet their lives on its
correctness.  For example, the astronauts bet their
lives that it would take four days to reach the
moon, that the performance required to land on
it was within the capability of the LEM and 
that their 300 pound life support systems really
would weigh only 50 pounds on the moon.  The Shuttle
astronauts bet their lives of the correctness of
the programs that control re-entry.